package AES
is
  MAXKC: constant Integer := 8;
  MAXNR: constant Integer := 14;

  type byte is mod 2 ** 8;
  type word is mod 2 ** 32;

  type word_table is array (byte) of word;
  subtype rcon_index is Integer range 0 .. 9;
  type rcon_array is array (rcon_index) of word;

--  Te0[x] = S [x].[02, 01, 01, 03];
--  Te1[x] = S [x].[03, 02, 01, 01];
--  Te2[x] = S [x].[01, 03, 02, 01];
--  Te3[x] = S [x].[01, 01, 03, 02];
--  Te4[x] = S [x].[01, 01, 01, 01];

--  Td0[x] = Si[x].[0e, 09, 0d, 0b];
--  Td1[x] = Si[x].[0b, 0e, 09, 0d];
--  Td2[x] = Si[x].[0d, 0b, 0e, 09];
--  Td3[x] = Si[x].[09, 0d, 0b, 0e];
--  Td4[x] = Si[x].[01, 01, 01, 01];

  Te0: constant word_table := word_table'(
    16#c66363a5#, 16#f87c7c84#, 16#ee777799#, 16#f67b7b8d#,
    16#fff2f20d#, 16#d66b6bbd#, 16#de6f6fb1#, 16#91c5c554#,
    16#60303050#, 16#02010103#, 16#ce6767a9#, 16#562b2b7d#,
    16#e7fefe19#, 16#b5d7d762#, 16#4dababe6#, 16#ec76769a#,
    16#8fcaca45#, 16#1f82829d#, 16#89c9c940#, 16#fa7d7d87#,
    16#effafa15#, 16#b25959eb#, 16#8e4747c9#, 16#fbf0f00b#,
    16#41adadec#, 16#b3d4d467#, 16#5fa2a2fd#, 16#45afafea#,
    16#239c9cbf#, 16#53a4a4f7#, 16#e4727296#, 16#9bc0c05b#,
    16#75b7b7c2#, 16#e1fdfd1c#, 16#3d9393ae#, 16#4c26266a#,
    16#6c36365a#, 16#7e3f3f41#, 16#f5f7f702#, 16#83cccc4f#,
    16#6834345c#, 16#51a5a5f4#, 16#d1e5e534#, 16#f9f1f108#,
    16#e2717193#, 16#abd8d873#, 16#62313153#, 16#2a15153f#,
    16#0804040c#, 16#95c7c752#, 16#46232365#, 16#9dc3c35e#,
    16#30181828#, 16#379696a1#, 16#0a05050f#, 16#2f9a9ab5#,
    16#0e070709#, 16#24121236#, 16#1b80809b#, 16#dfe2e23d#,
    16#cdebeb26#, 16#4e272769#, 16#7fb2b2cd#, 16#ea75759f#,
    16#1209091b#, 16#1d83839e#, 16#582c2c74#, 16#341a1a2e#,
    16#361b1b2d#, 16#dc6e6eb2#, 16#b45a5aee#, 16#5ba0a0fb#,
    16#a45252f6#, 16#763b3b4d#, 16#b7d6d661#, 16#7db3b3ce#,
    16#5229297b#, 16#dde3e33e#, 16#5e2f2f71#, 16#13848497#,
    16#a65353f5#, 16#b9d1d168#, 16#00000000#, 16#c1eded2c#,
    16#40202060#, 16#e3fcfc1f#, 16#79b1b1c8#, 16#b65b5bed#,
    16#d46a6abe#, 16#8dcbcb46#, 16#67bebed9#, 16#7239394b#,
    16#944a4ade#, 16#984c4cd4#, 16#b05858e8#, 16#85cfcf4a#,
    16#bbd0d06b#, 16#c5efef2a#, 16#4faaaae5#, 16#edfbfb16#,
    16#864343c5#, 16#9a4d4dd7#, 16#66333355#, 16#11858594#,
    16#8a4545cf#, 16#e9f9f910#, 16#04020206#, 16#fe7f7f81#,
    16#a05050f0#, 16#783c3c44#, 16#259f9fba#, 16#4ba8a8e3#,
    16#a25151f3#, 16#5da3a3fe#, 16#804040c0#, 16#058f8f8a#,
    16#3f9292ad#, 16#219d9dbc#, 16#70383848#, 16#f1f5f504#,
    16#63bcbcdf#, 16#77b6b6c1#, 16#afdada75#, 16#42212163#,
    16#20101030#, 16#e5ffff1a#, 16#fdf3f30e#, 16#bfd2d26d#,
    16#81cdcd4c#, 16#180c0c14#, 16#26131335#, 16#c3ecec2f#,
    16#be5f5fe1#, 16#359797a2#, 16#884444cc#, 16#2e171739#,
    16#93c4c457#, 16#55a7a7f2#, 16#fc7e7e82#, 16#7a3d3d47#,
    16#c86464ac#, 16#ba5d5de7#, 16#3219192b#, 16#e6737395#,
    16#c06060a0#, 16#19818198#, 16#9e4f4fd1#, 16#a3dcdc7f#,
    16#44222266#, 16#542a2a7e#, 16#3b9090ab#, 16#0b888883#,
    16#8c4646ca#, 16#c7eeee29#, 16#6bb8b8d3#, 16#2814143c#,
    16#a7dede79#, 16#bc5e5ee2#, 16#160b0b1d#, 16#addbdb76#,
    16#dbe0e03b#, 16#64323256#, 16#743a3a4e#, 16#140a0a1e#,
    16#924949db#, 16#0c06060a#, 16#4824246c#, 16#b85c5ce4#,
    16#9fc2c25d#, 16#bdd3d36e#, 16#43acacef#, 16#c46262a6#,
    16#399191a8#, 16#319595a4#, 16#d3e4e437#, 16#f279798b#,
    16#d5e7e732#, 16#8bc8c843#, 16#6e373759#, 16#da6d6db7#,
    16#018d8d8c#, 16#b1d5d564#, 16#9c4e4ed2#, 16#49a9a9e0#,
    16#d86c6cb4#, 16#ac5656fa#, 16#f3f4f407#, 16#cfeaea25#,
    16#ca6565af#, 16#f47a7a8e#, 16#47aeaee9#, 16#10080818#,
    16#6fbabad5#, 16#f0787888#, 16#4a25256f#, 16#5c2e2e72#,
    16#381c1c24#, 16#57a6a6f1#, 16#73b4b4c7#, 16#97c6c651#,
    16#cbe8e823#, 16#a1dddd7c#, 16#e874749c#, 16#3e1f1f21#,
    16#964b4bdd#, 16#61bdbddc#, 16#0d8b8b86#, 16#0f8a8a85#,
    16#e0707090#, 16#7c3e3e42#, 16#71b5b5c4#, 16#cc6666aa#,
    16#904848d8#, 16#06030305#, 16#f7f6f601#, 16#1c0e0e12#,
    16#c26161a3#, 16#6a35355f#, 16#ae5757f9#, 16#69b9b9d0#,
    16#17868691#, 16#99c1c158#, 16#3a1d1d27#, 16#279e9eb9#,
    16#d9e1e138#, 16#ebf8f813#, 16#2b9898b3#, 16#22111133#,
    16#d26969bb#, 16#a9d9d970#, 16#078e8e89#, 16#339494a7#,
    16#2d9b9bb6#, 16#3c1e1e22#, 16#15878792#, 16#c9e9e920#,
    16#87cece49#, 16#aa5555ff#, 16#50282878#, 16#a5dfdf7a#,
    16#038c8c8f#, 16#59a1a1f8#, 16#09898980#, 16#1a0d0d17#,
    16#65bfbfda#, 16#d7e6e631#, 16#844242c6#, 16#d06868b8#,
    16#824141c3#, 16#299999b0#, 16#5a2d2d77#, 16#1e0f0f11#,
    16#7bb0b0cb#, 16#a85454fc#, 16#6dbbbbd6#, 16#2c16163a#
  );

  Te1: constant word_table := word_table'(
    16#a5c66363#, 16#84f87c7c#, 16#99ee7777#, 16#8df67b7b#,
    16#0dfff2f2#, 16#bdd66b6b#, 16#b1de6f6f#, 16#5491c5c5#,
    16#50603030#, 16#03020101#, 16#a9ce6767#, 16#7d562b2b#,
    16#19e7fefe#, 16#62b5d7d7#, 16#e64dabab#, 16#9aec7676#,
    16#458fcaca#, 16#9d1f8282#, 16#4089c9c9#, 16#87fa7d7d#,
    16#15effafa#, 16#ebb25959#, 16#c98e4747#, 16#0bfbf0f0#,
    16#ec41adad#, 16#67b3d4d4#, 16#fd5fa2a2#, 16#ea45afaf#,
    16#bf239c9c#, 16#f753a4a4#, 16#96e47272#, 16#5b9bc0c0#,
    16#c275b7b7#, 16#1ce1fdfd#, 16#ae3d9393#, 16#6a4c2626#,
    16#5a6c3636#, 16#417e3f3f#, 16#02f5f7f7#, 16#4f83cccc#,
    16#5c683434#, 16#f451a5a5#, 16#34d1e5e5#, 16#08f9f1f1#,
    16#93e27171#, 16#73abd8d8#, 16#53623131#, 16#3f2a1515#,
    16#0c080404#, 16#5295c7c7#, 16#65462323#, 16#5e9dc3c3#,
    16#28301818#, 16#a1379696#, 16#0f0a0505#, 16#b52f9a9a#,
    16#090e0707#, 16#36241212#, 16#9b1b8080#, 16#3ddfe2e2#,
    16#26cdebeb#, 16#694e2727#, 16#cd7fb2b2#, 16#9fea7575#,
    16#1b120909#, 16#9e1d8383#, 16#74582c2c#, 16#2e341a1a#,
    16#2d361b1b#, 16#b2dc6e6e#, 16#eeb45a5a#, 16#fb5ba0a0#,
    16#f6a45252#, 16#4d763b3b#, 16#61b7d6d6#, 16#ce7db3b3#,
    16#7b522929#, 16#3edde3e3#, 16#715e2f2f#, 16#97138484#,
    16#f5a65353#, 16#68b9d1d1#, 16#00000000#, 16#2cc1eded#,
    16#60402020#, 16#1fe3fcfc#, 16#c879b1b1#, 16#edb65b5b#,
    16#bed46a6a#, 16#468dcbcb#, 16#d967bebe#, 16#4b723939#,
    16#de944a4a#, 16#d4984c4c#, 16#e8b05858#, 16#4a85cfcf#,
    16#6bbbd0d0#, 16#2ac5efef#, 16#e54faaaa#, 16#16edfbfb#,
    16#c5864343#, 16#d79a4d4d#, 16#55663333#, 16#94118585#,
    16#cf8a4545#, 16#10e9f9f9#, 16#06040202#, 16#81fe7f7f#,
    16#f0a05050#, 16#44783c3c#, 16#ba259f9f#, 16#e34ba8a8#,
    16#f3a25151#, 16#fe5da3a3#, 16#c0804040#, 16#8a058f8f#,
    16#ad3f9292#, 16#bc219d9d#, 16#48703838#, 16#04f1f5f5#,
    16#df63bcbc#, 16#c177b6b6#, 16#75afdada#, 16#63422121#,
    16#30201010#, 16#1ae5ffff#, 16#0efdf3f3#, 16#6dbfd2d2#,
    16#4c81cdcd#, 16#14180c0c#, 16#35261313#, 16#2fc3ecec#,
    16#e1be5f5f#, 16#a2359797#, 16#cc884444#, 16#392e1717#,
    16#5793c4c4#, 16#f255a7a7#, 16#82fc7e7e#, 16#477a3d3d#,
    16#acc86464#, 16#e7ba5d5d#, 16#2b321919#, 16#95e67373#,
    16#a0c06060#, 16#98198181#, 16#d19e4f4f#, 16#7fa3dcdc#,
    16#66442222#, 16#7e542a2a#, 16#ab3b9090#, 16#830b8888#,
    16#ca8c4646#, 16#29c7eeee#, 16#d36bb8b8#, 16#3c281414#,
    16#79a7dede#, 16#e2bc5e5e#, 16#1d160b0b#, 16#76addbdb#,
    16#3bdbe0e0#, 16#56643232#, 16#4e743a3a#, 16#1e140a0a#,
    16#db924949#, 16#0a0c0606#, 16#6c482424#, 16#e4b85c5c#,
    16#5d9fc2c2#, 16#6ebdd3d3#, 16#ef43acac#, 16#a6c46262#,
    16#a8399191#, 16#a4319595#, 16#37d3e4e4#, 16#8bf27979#,
    16#32d5e7e7#, 16#438bc8c8#, 16#596e3737#, 16#b7da6d6d#,
    16#8c018d8d#, 16#64b1d5d5#, 16#d29c4e4e#, 16#e049a9a9#,
    16#b4d86c6c#, 16#faac5656#, 16#07f3f4f4#, 16#25cfeaea#,
    16#afca6565#, 16#8ef47a7a#, 16#e947aeae#, 16#18100808#,
    16#d56fbaba#, 16#88f07878#, 16#6f4a2525#, 16#725c2e2e#,
    16#24381c1c#, 16#f157a6a6#, 16#c773b4b4#, 16#5197c6c6#,
    16#23cbe8e8#, 16#7ca1dddd#, 16#9ce87474#, 16#213e1f1f#,
    16#dd964b4b#, 16#dc61bdbd#, 16#860d8b8b#, 16#850f8a8a#,
    16#90e07070#, 16#427c3e3e#, 16#c471b5b5#, 16#aacc6666#,
    16#d8904848#, 16#05060303#, 16#01f7f6f6#, 16#121c0e0e#,
    16#a3c26161#, 16#5f6a3535#, 16#f9ae5757#, 16#d069b9b9#,
    16#91178686#, 16#5899c1c1#, 16#273a1d1d#, 16#b9279e9e#,
    16#38d9e1e1#, 16#13ebf8f8#, 16#b32b9898#, 16#33221111#,
    16#bbd26969#, 16#70a9d9d9#, 16#89078e8e#, 16#a7339494#,
    16#b62d9b9b#, 16#223c1e1e#, 16#92158787#, 16#20c9e9e9#,
    16#4987cece#, 16#ffaa5555#, 16#78502828#, 16#7aa5dfdf#,
    16#8f038c8c#, 16#f859a1a1#, 16#80098989#, 16#171a0d0d#,
    16#da65bfbf#, 16#31d7e6e6#, 16#c6844242#, 16#b8d06868#,
    16#c3824141#, 16#b0299999#, 16#775a2d2d#, 16#111e0f0f#,
    16#cb7bb0b0#, 16#fca85454#, 16#d66dbbbb#, 16#3a2c1616#
  );

  Te2: constant word_table := word_table'(
    16#63a5c663#, 16#7c84f87c#, 16#7799ee77#, 16#7b8df67b#,
    16#f20dfff2#, 16#6bbdd66b#, 16#6fb1de6f#, 16#c55491c5#,
    16#30506030#, 16#01030201#, 16#67a9ce67#, 16#2b7d562b#,
    16#fe19e7fe#, 16#d762b5d7#, 16#abe64dab#, 16#769aec76#,
    16#ca458fca#, 16#829d1f82#, 16#c94089c9#, 16#7d87fa7d#,
    16#fa15effa#, 16#59ebb259#, 16#47c98e47#, 16#f00bfbf0#,
    16#adec41ad#, 16#d467b3d4#, 16#a2fd5fa2#, 16#afea45af#,
    16#9cbf239c#, 16#a4f753a4#, 16#7296e472#, 16#c05b9bc0#,
    16#b7c275b7#, 16#fd1ce1fd#, 16#93ae3d93#, 16#266a4c26#,
    16#365a6c36#, 16#3f417e3f#, 16#f702f5f7#, 16#cc4f83cc#,
    16#345c6834#, 16#a5f451a5#, 16#e534d1e5#, 16#f108f9f1#,
    16#7193e271#, 16#d873abd8#, 16#31536231#, 16#153f2a15#,
    16#040c0804#, 16#c75295c7#, 16#23654623#, 16#c35e9dc3#,
    16#18283018#, 16#96a13796#, 16#050f0a05#, 16#9ab52f9a#,
    16#07090e07#, 16#12362412#, 16#809b1b80#, 16#e23ddfe2#,
    16#eb26cdeb#, 16#27694e27#, 16#b2cd7fb2#, 16#759fea75#,
    16#091b1209#, 16#839e1d83#, 16#2c74582c#, 16#1a2e341a#,
    16#1b2d361b#, 16#6eb2dc6e#, 16#5aeeb45a#, 16#a0fb5ba0#,
    16#52f6a452#, 16#3b4d763b#, 16#d661b7d6#, 16#b3ce7db3#,
    16#297b5229#, 16#e33edde3#, 16#2f715e2f#, 16#84971384#,
    16#53f5a653#, 16#d168b9d1#, 16#00000000#, 16#ed2cc1ed#,
    16#20604020#, 16#fc1fe3fc#, 16#b1c879b1#, 16#5bedb65b#,
    16#6abed46a#, 16#cb468dcb#, 16#bed967be#, 16#394b7239#,
    16#4ade944a#, 16#4cd4984c#, 16#58e8b058#, 16#cf4a85cf#,
    16#d06bbbd0#, 16#ef2ac5ef#, 16#aae54faa#, 16#fb16edfb#,
    16#43c58643#, 16#4dd79a4d#, 16#33556633#, 16#85941185#,
    16#45cf8a45#, 16#f910e9f9#, 16#02060402#, 16#7f81fe7f#,
    16#50f0a050#, 16#3c44783c#, 16#9fba259f#, 16#a8e34ba8#,
    16#51f3a251#, 16#a3fe5da3#, 16#40c08040#, 16#8f8a058f#,
    16#92ad3f92#, 16#9dbc219d#, 16#38487038#, 16#f504f1f5#,
    16#bcdf63bc#, 16#b6c177b6#, 16#da75afda#, 16#21634221#,
    16#10302010#, 16#ff1ae5ff#, 16#f30efdf3#, 16#d26dbfd2#,
    16#cd4c81cd#, 16#0c14180c#, 16#13352613#, 16#ec2fc3ec#,
    16#5fe1be5f#, 16#97a23597#, 16#44cc8844#, 16#17392e17#,
    16#c45793c4#, 16#a7f255a7#, 16#7e82fc7e#, 16#3d477a3d#,
    16#64acc864#, 16#5de7ba5d#, 16#192b3219#, 16#7395e673#,
    16#60a0c060#, 16#81981981#, 16#4fd19e4f#, 16#dc7fa3dc#,
    16#22664422#, 16#2a7e542a#, 16#90ab3b90#, 16#88830b88#,
    16#46ca8c46#, 16#ee29c7ee#, 16#b8d36bb8#, 16#143c2814#,
    16#de79a7de#, 16#5ee2bc5e#, 16#0b1d160b#, 16#db76addb#,
    16#e03bdbe0#, 16#32566432#, 16#3a4e743a#, 16#0a1e140a#,
    16#49db9249#, 16#060a0c06#, 16#246c4824#, 16#5ce4b85c#,
    16#c25d9fc2#, 16#d36ebdd3#, 16#acef43ac#, 16#62a6c462#,
    16#91a83991#, 16#95a43195#, 16#e437d3e4#, 16#798bf279#,
    16#e732d5e7#, 16#c8438bc8#, 16#37596e37#, 16#6db7da6d#,
    16#8d8c018d#, 16#d564b1d5#, 16#4ed29c4e#, 16#a9e049a9#,
    16#6cb4d86c#, 16#56faac56#, 16#f407f3f4#, 16#ea25cfea#,
    16#65afca65#, 16#7a8ef47a#, 16#aee947ae#, 16#08181008#,
    16#bad56fba#, 16#7888f078#, 16#256f4a25#, 16#2e725c2e#,
    16#1c24381c#, 16#a6f157a6#, 16#b4c773b4#, 16#c65197c6#,
    16#e823cbe8#, 16#dd7ca1dd#, 16#749ce874#, 16#1f213e1f#,
    16#4bdd964b#, 16#bddc61bd#, 16#8b860d8b#, 16#8a850f8a#,
    16#7090e070#, 16#3e427c3e#, 16#b5c471b5#, 16#66aacc66#,
    16#48d89048#, 16#03050603#, 16#f601f7f6#, 16#0e121c0e#,
    16#61a3c261#, 16#355f6a35#, 16#57f9ae57#, 16#b9d069b9#,
    16#86911786#, 16#c15899c1#, 16#1d273a1d#, 16#9eb9279e#,
    16#e138d9e1#, 16#f813ebf8#, 16#98b32b98#, 16#11332211#,
    16#69bbd269#, 16#d970a9d9#, 16#8e89078e#, 16#94a73394#,
    16#9bb62d9b#, 16#1e223c1e#, 16#87921587#, 16#e920c9e9#,
    16#ce4987ce#, 16#55ffaa55#, 16#28785028#, 16#df7aa5df#,
    16#8c8f038c#, 16#a1f859a1#, 16#89800989#, 16#0d171a0d#,
    16#bfda65bf#, 16#e631d7e6#, 16#42c68442#, 16#68b8d068#,
    16#41c38241#, 16#99b02999#, 16#2d775a2d#, 16#0f111e0f#,
    16#b0cb7bb0#, 16#54fca854#, 16#bbd66dbb#, 16#163a2c16#
  );

  Te3: constant word_table := word_table'(
    16#6363a5c6#, 16#7c7c84f8#, 16#777799ee#, 16#7b7b8df6#,
    16#f2f20dff#, 16#6b6bbdd6#, 16#6f6fb1de#, 16#c5c55491#,
    16#30305060#, 16#01010302#, 16#6767a9ce#, 16#2b2b7d56#,
    16#fefe19e7#, 16#d7d762b5#, 16#ababe64d#, 16#76769aec#,
    16#caca458f#, 16#82829d1f#, 16#c9c94089#, 16#7d7d87fa#,
    16#fafa15ef#, 16#5959ebb2#, 16#4747c98e#, 16#f0f00bfb#,
    16#adadec41#, 16#d4d467b3#, 16#a2a2fd5f#, 16#afafea45#,
    16#9c9cbf23#, 16#a4a4f753#, 16#727296e4#, 16#c0c05b9b#,
    16#b7b7c275#, 16#fdfd1ce1#, 16#9393ae3d#, 16#26266a4c#,
    16#36365a6c#, 16#3f3f417e#, 16#f7f702f5#, 16#cccc4f83#,
    16#34345c68#, 16#a5a5f451#, 16#e5e534d1#, 16#f1f108f9#,
    16#717193e2#, 16#d8d873ab#, 16#31315362#, 16#15153f2a#,
    16#04040c08#, 16#c7c75295#, 16#23236546#, 16#c3c35e9d#,
    16#18182830#, 16#9696a137#, 16#05050f0a#, 16#9a9ab52f#,
    16#0707090e#, 16#12123624#, 16#80809b1b#, 16#e2e23ddf#,
    16#ebeb26cd#, 16#2727694e#, 16#b2b2cd7f#, 16#75759fea#,
    16#09091b12#, 16#83839e1d#, 16#2c2c7458#, 16#1a1a2e34#,
    16#1b1b2d36#, 16#6e6eb2dc#, 16#5a5aeeb4#, 16#a0a0fb5b#,
    16#5252f6a4#, 16#3b3b4d76#, 16#d6d661b7#, 16#b3b3ce7d#,
    16#29297b52#, 16#e3e33edd#, 16#2f2f715e#, 16#84849713#,
    16#5353f5a6#, 16#d1d168b9#, 16#00000000#, 16#eded2cc1#,
    16#20206040#, 16#fcfc1fe3#, 16#b1b1c879#, 16#5b5bedb6#,
    16#6a6abed4#, 16#cbcb468d#, 16#bebed967#, 16#39394b72#,
    16#4a4ade94#, 16#4c4cd498#, 16#5858e8b0#, 16#cfcf4a85#,
    16#d0d06bbb#, 16#efef2ac5#, 16#aaaae54f#, 16#fbfb16ed#,
    16#4343c586#, 16#4d4dd79a#, 16#33335566#, 16#85859411#,
    16#4545cf8a#, 16#f9f910e9#, 16#02020604#, 16#7f7f81fe#,
    16#5050f0a0#, 16#3c3c4478#, 16#9f9fba25#, 16#a8a8e34b#,
    16#5151f3a2#, 16#a3a3fe5d#, 16#4040c080#, 16#8f8f8a05#,
    16#9292ad3f#, 16#9d9dbc21#, 16#38384870#, 16#f5f504f1#,
    16#bcbcdf63#, 16#b6b6c177#, 16#dada75af#, 16#21216342#,
    16#10103020#, 16#ffff1ae5#, 16#f3f30efd#, 16#d2d26dbf#,
    16#cdcd4c81#, 16#0c0c1418#, 16#13133526#, 16#ecec2fc3#,
    16#5f5fe1be#, 16#9797a235#, 16#4444cc88#, 16#1717392e#,
    16#c4c45793#, 16#a7a7f255#, 16#7e7e82fc#, 16#3d3d477a#,
    16#6464acc8#, 16#5d5de7ba#, 16#19192b32#, 16#737395e6#,
    16#6060a0c0#, 16#81819819#, 16#4f4fd19e#, 16#dcdc7fa3#,
    16#22226644#, 16#2a2a7e54#, 16#9090ab3b#, 16#8888830b#,
    16#4646ca8c#, 16#eeee29c7#, 16#b8b8d36b#, 16#14143c28#,
    16#dede79a7#, 16#5e5ee2bc#, 16#0b0b1d16#, 16#dbdb76ad#,
    16#e0e03bdb#, 16#32325664#, 16#3a3a4e74#, 16#0a0a1e14#,
    16#4949db92#, 16#06060a0c#, 16#24246c48#, 16#5c5ce4b8#,
    16#c2c25d9f#, 16#d3d36ebd#, 16#acacef43#, 16#6262a6c4#,
    16#9191a839#, 16#9595a431#, 16#e4e437d3#, 16#79798bf2#,
    16#e7e732d5#, 16#c8c8438b#, 16#3737596e#, 16#6d6db7da#,
    16#8d8d8c01#, 16#d5d564b1#, 16#4e4ed29c#, 16#a9a9e049#,
    16#6c6cb4d8#, 16#5656faac#, 16#f4f407f3#, 16#eaea25cf#,
    16#6565afca#, 16#7a7a8ef4#, 16#aeaee947#, 16#08081810#,
    16#babad56f#, 16#787888f0#, 16#25256f4a#, 16#2e2e725c#,
    16#1c1c2438#, 16#a6a6f157#, 16#b4b4c773#, 16#c6c65197#,
    16#e8e823cb#, 16#dddd7ca1#, 16#74749ce8#, 16#1f1f213e#,
    16#4b4bdd96#, 16#bdbddc61#, 16#8b8b860d#, 16#8a8a850f#,
    16#707090e0#, 16#3e3e427c#, 16#b5b5c471#, 16#6666aacc#,
    16#4848d890#, 16#03030506#, 16#f6f601f7#, 16#0e0e121c#,
    16#6161a3c2#, 16#35355f6a#, 16#5757f9ae#, 16#b9b9d069#,
    16#86869117#, 16#c1c15899#, 16#1d1d273a#, 16#9e9eb927#,
    16#e1e138d9#, 16#f8f813eb#, 16#9898b32b#, 16#11113322#,
    16#6969bbd2#, 16#d9d970a9#, 16#8e8e8907#, 16#9494a733#,
    16#9b9bb62d#, 16#1e1e223c#, 16#87879215#, 16#e9e920c9#,
    16#cece4987#, 16#5555ffaa#, 16#28287850#, 16#dfdf7aa5#,
    16#8c8c8f03#, 16#a1a1f859#, 16#89898009#, 16#0d0d171a#,
    16#bfbfda65#, 16#e6e631d7#, 16#4242c684#, 16#6868b8d0#,
    16#4141c382#, 16#9999b029#, 16#2d2d775a#, 16#0f0f111e#,
    16#b0b0cb7b#, 16#5454fca8#, 16#bbbbd66d#, 16#16163a2c#
  );
  
  Te4: constant word_table := word_table'(
    16#63636363#, 16#7c7c7c7c#, 16#77777777#, 16#7b7b7b7b#,
    16#f2f2f2f2#, 16#6b6b6b6b#, 16#6f6f6f6f#, 16#c5c5c5c5#,
    16#30303030#, 16#01010101#, 16#67676767#, 16#2b2b2b2b#,
    16#fefefefe#, 16#d7d7d7d7#, 16#abababab#, 16#76767676#,
    16#cacacaca#, 16#82828282#, 16#c9c9c9c9#, 16#7d7d7d7d#,
    16#fafafafa#, 16#59595959#, 16#47474747#, 16#f0f0f0f0#,
    16#adadadad#, 16#d4d4d4d4#, 16#a2a2a2a2#, 16#afafafaf#,
    16#9c9c9c9c#, 16#a4a4a4a4#, 16#72727272#, 16#c0c0c0c0#,
    16#b7b7b7b7#, 16#fdfdfdfd#, 16#93939393#, 16#26262626#,
    16#36363636#, 16#3f3f3f3f#, 16#f7f7f7f7#, 16#cccccccc#,
    16#34343434#, 16#a5a5a5a5#, 16#e5e5e5e5#, 16#f1f1f1f1#,
    16#71717171#, 16#d8d8d8d8#, 16#31313131#, 16#15151515#,
    16#04040404#, 16#c7c7c7c7#, 16#23232323#, 16#c3c3c3c3#,
    16#18181818#, 16#96969696#, 16#05050505#, 16#9a9a9a9a#,
    16#07070707#, 16#12121212#, 16#80808080#, 16#e2e2e2e2#,
    16#ebebebeb#, 16#27272727#, 16#b2b2b2b2#, 16#75757575#,
    16#09090909#, 16#83838383#, 16#2c2c2c2c#, 16#1a1a1a1a#,
    16#1b1b1b1b#, 16#6e6e6e6e#, 16#5a5a5a5a#, 16#a0a0a0a0#,
    16#52525252#, 16#3b3b3b3b#, 16#d6d6d6d6#, 16#b3b3b3b3#,
    16#29292929#, 16#e3e3e3e3#, 16#2f2f2f2f#, 16#84848484#,
    16#53535353#, 16#d1d1d1d1#, 16#00000000#, 16#edededed#,
    16#20202020#, 16#fcfcfcfc#, 16#b1b1b1b1#, 16#5b5b5b5b#,
    16#6a6a6a6a#, 16#cbcbcbcb#, 16#bebebebe#, 16#39393939#,
    16#4a4a4a4a#, 16#4c4c4c4c#, 16#58585858#, 16#cfcfcfcf#,
    16#d0d0d0d0#, 16#efefefef#, 16#aaaaaaaa#, 16#fbfbfbfb#,
    16#43434343#, 16#4d4d4d4d#, 16#33333333#, 16#85858585#,
    16#45454545#, 16#f9f9f9f9#, 16#02020202#, 16#7f7f7f7f#,
    16#50505050#, 16#3c3c3c3c#, 16#9f9f9f9f#, 16#a8a8a8a8#,
    16#51515151#, 16#a3a3a3a3#, 16#40404040#, 16#8f8f8f8f#,
    16#92929292#, 16#9d9d9d9d#, 16#38383838#, 16#f5f5f5f5#,
    16#bcbcbcbc#, 16#b6b6b6b6#, 16#dadadada#, 16#21212121#,
    16#10101010#, 16#ffffffff#, 16#f3f3f3f3#, 16#d2d2d2d2#,
    16#cdcdcdcd#, 16#0c0c0c0c#, 16#13131313#, 16#ecececec#,
    16#5f5f5f5f#, 16#97979797#, 16#44444444#, 16#17171717#,
    16#c4c4c4c4#, 16#a7a7a7a7#, 16#7e7e7e7e#, 16#3d3d3d3d#,
    16#64646464#, 16#5d5d5d5d#, 16#19191919#, 16#73737373#,
    16#60606060#, 16#81818181#, 16#4f4f4f4f#, 16#dcdcdcdc#,
    16#22222222#, 16#2a2a2a2a#, 16#90909090#, 16#88888888#,
    16#46464646#, 16#eeeeeeee#, 16#b8b8b8b8#, 16#14141414#,
    16#dededede#, 16#5e5e5e5e#, 16#0b0b0b0b#, 16#dbdbdbdb#,
    16#e0e0e0e0#, 16#32323232#, 16#3a3a3a3a#, 16#0a0a0a0a#,
    16#49494949#, 16#06060606#, 16#24242424#, 16#5c5c5c5c#,
    16#c2c2c2c2#, 16#d3d3d3d3#, 16#acacacac#, 16#62626262#,
    16#91919191#, 16#95959595#, 16#e4e4e4e4#, 16#79797979#,
    16#e7e7e7e7#, 16#c8c8c8c8#, 16#37373737#, 16#6d6d6d6d#,
    16#8d8d8d8d#, 16#d5d5d5d5#, 16#4e4e4e4e#, 16#a9a9a9a9#,
    16#6c6c6c6c#, 16#56565656#, 16#f4f4f4f4#, 16#eaeaeaea#,
    16#65656565#, 16#7a7a7a7a#, 16#aeaeaeae#, 16#08080808#,
    16#babababa#, 16#78787878#, 16#25252525#, 16#2e2e2e2e#,
    16#1c1c1c1c#, 16#a6a6a6a6#, 16#b4b4b4b4#, 16#c6c6c6c6#,
    16#e8e8e8e8#, 16#dddddddd#, 16#74747474#, 16#1f1f1f1f#,
    16#4b4b4b4b#, 16#bdbdbdbd#, 16#8b8b8b8b#, 16#8a8a8a8a#,
    16#70707070#, 16#3e3e3e3e#, 16#b5b5b5b5#, 16#66666666#,
    16#48484848#, 16#03030303#, 16#f6f6f6f6#, 16#0e0e0e0e#,
    16#61616161#, 16#35353535#, 16#57575757#, 16#b9b9b9b9#,
    16#86868686#, 16#c1c1c1c1#, 16#1d1d1d1d#, 16#9e9e9e9e#,
    16#e1e1e1e1#, 16#f8f8f8f8#, 16#98989898#, 16#11111111#,
    16#69696969#, 16#d9d9d9d9#, 16#8e8e8e8e#, 16#94949494#,
    16#9b9b9b9b#, 16#1e1e1e1e#, 16#87878787#, 16#e9e9e9e9#,
    16#cececece#, 16#55555555#, 16#28282828#, 16#dfdfdfdf#,
    16#8c8c8c8c#, 16#a1a1a1a1#, 16#89898989#, 16#0d0d0d0d#,
    16#bfbfbfbf#, 16#e6e6e6e6#, 16#42424242#, 16#68686868#,
    16#41414141#, 16#99999999#, 16#2d2d2d2d#, 16#0f0f0f0f#,
    16#b0b0b0b0#, 16#54545454#, 16#bbbbbbbb#, 16#16161616#
  );
  
  Td0: constant word_table := word_table'(
    16#51f4a750#, 16#7e416553#, 16#1a17a4c3#, 16#3a275e96#,
    16#3bab6bcb#, 16#1f9d45f1#, 16#acfa58ab#, 16#4be30393#,
    16#2030fa55#, 16#ad766df6#, 16#88cc7691#, 16#f5024c25#,
    16#4fe5d7fc#, 16#c52acbd7#, 16#26354480#, 16#b562a38f#,
    16#deb15a49#, 16#25ba1b67#, 16#45ea0e98#, 16#5dfec0e1#,
    16#c32f7502#, 16#814cf012#, 16#8d4697a3#, 16#6bd3f9c6#,
    16#038f5fe7#, 16#15929c95#, 16#bf6d7aeb#, 16#955259da#,
    16#d4be832d#, 16#587421d3#, 16#49e06929#, 16#8ec9c844#,
    16#75c2896a#, 16#f48e7978#, 16#99583e6b#, 16#27b971dd#,
    16#bee14fb6#, 16#f088ad17#, 16#c920ac66#, 16#7dce3ab4#,
    16#63df4a18#, 16#e51a3182#, 16#97513360#, 16#62537f45#,
    16#b16477e0#, 16#bb6bae84#, 16#fe81a01c#, 16#f9082b94#,
    16#70486858#, 16#8f45fd19#, 16#94de6c87#, 16#527bf8b7#,
    16#ab73d323#, 16#724b02e2#, 16#e31f8f57#, 16#6655ab2a#,
    16#b2eb2807#, 16#2fb5c203#, 16#86c57b9a#, 16#d33708a5#,
    16#302887f2#, 16#23bfa5b2#, 16#02036aba#, 16#ed16825c#,
    16#8acf1c2b#, 16#a779b492#, 16#f307f2f0#, 16#4e69e2a1#,
    16#65daf4cd#, 16#0605bed5#, 16#d134621f#, 16#c4a6fe8a#,
    16#342e539d#, 16#a2f355a0#, 16#058ae132#, 16#a4f6eb75#,
    16#0b83ec39#, 16#4060efaa#, 16#5e719f06#, 16#bd6e1051#,
    16#3e218af9#, 16#96dd063d#, 16#dd3e05ae#, 16#4de6bd46#,
    16#91548db5#, 16#71c45d05#, 16#0406d46f#, 16#605015ff#,
    16#1998fb24#, 16#d6bde997#, 16#894043cc#, 16#67d99e77#,
    16#b0e842bd#, 16#07898b88#, 16#e7195b38#, 16#79c8eedb#,
    16#a17c0a47#, 16#7c420fe9#, 16#f8841ec9#, 16#00000000#,
    16#09808683#, 16#322bed48#, 16#1e1170ac#, 16#6c5a724e#,
    16#fd0efffb#, 16#0f853856#, 16#3daed51e#, 16#362d3927#,
    16#0a0fd964#, 16#685ca621#, 16#9b5b54d1#, 16#24362e3a#,
    16#0c0a67b1#, 16#9357e70f#, 16#b4ee96d2#, 16#1b9b919e#,
    16#80c0c54f#, 16#61dc20a2#, 16#5a774b69#, 16#1c121a16#,
    16#e293ba0a#, 16#c0a02ae5#, 16#3c22e043#, 16#121b171d#,
    16#0e090d0b#, 16#f28bc7ad#, 16#2db6a8b9#, 16#141ea9c8#,
    16#57f11985#, 16#af75074c#, 16#ee99ddbb#, 16#a37f60fd#,
    16#f701269f#, 16#5c72f5bc#, 16#44663bc5#, 16#5bfb7e34#,
    16#8b432976#, 16#cb23c6dc#, 16#b6edfc68#, 16#b8e4f163#,
    16#d731dcca#, 16#42638510#, 16#13972240#, 16#84c61120#,
    16#854a247d#, 16#d2bb3df8#, 16#aef93211#, 16#c729a16d#,
    16#1d9e2f4b#, 16#dcb230f3#, 16#0d8652ec#, 16#77c1e3d0#,
    16#2bb3166c#, 16#a970b999#, 16#119448fa#, 16#47e96422#,
    16#a8fc8cc4#, 16#a0f03f1a#, 16#567d2cd8#, 16#223390ef#,
    16#87494ec7#, 16#d938d1c1#, 16#8ccaa2fe#, 16#98d40b36#,
    16#a6f581cf#, 16#a57ade28#, 16#dab78e26#, 16#3fadbfa4#,
    16#2c3a9de4#, 16#5078920d#, 16#6a5fcc9b#, 16#547e4662#,
    16#f68d13c2#, 16#90d8b8e8#, 16#2e39f75e#, 16#82c3aff5#,
    16#9f5d80be#, 16#69d0937c#, 16#6fd52da9#, 16#cf2512b3#,
    16#c8ac993b#, 16#10187da7#, 16#e89c636e#, 16#db3bbb7b#,
    16#cd267809#, 16#6e5918f4#, 16#ec9ab701#, 16#834f9aa8#,
    16#e6956e65#, 16#aaffe67e#, 16#21bccf08#, 16#ef15e8e6#,
    16#bae79bd9#, 16#4a6f36ce#, 16#ea9f09d4#, 16#29b07cd6#,
    16#31a4b2af#, 16#2a3f2331#, 16#c6a59430#, 16#35a266c0#,
    16#744ebc37#, 16#fc82caa6#, 16#e090d0b0#, 16#33a7d815#,
    16#f104984a#, 16#41ecdaf7#, 16#7fcd500e#, 16#1791f62f#,
    16#764dd68d#, 16#43efb04d#, 16#ccaa4d54#, 16#e49604df#,
    16#9ed1b5e3#, 16#4c6a881b#, 16#c12c1fb8#, 16#4665517f#,
    16#9d5eea04#, 16#018c355d#, 16#fa877473#, 16#fb0b412e#,
    16#b3671d5a#, 16#92dbd252#, 16#e9105633#, 16#6dd64713#,
    16#9ad7618c#, 16#37a10c7a#, 16#59f8148e#, 16#eb133c89#,
    16#cea927ee#, 16#b761c935#, 16#e11ce5ed#, 16#7a47b13c#,
    16#9cd2df59#, 16#55f2733f#, 16#1814ce79#, 16#73c737bf#,
    16#53f7cdea#, 16#5ffdaa5b#, 16#df3d6f14#, 16#7844db86#,
    16#caaff381#, 16#b968c43e#, 16#3824342c#, 16#c2a3405f#,
    16#161dc372#, 16#bce2250c#, 16#283c498b#, 16#ff0d9541#,
    16#39a80171#, 16#080cb3de#, 16#d8b4e49c#, 16#6456c190#,
    16#7bcb8461#, 16#d532b670#, 16#486c5c74#, 16#d0b85742#
  );
  
  Td1: constant word_table := word_table'(
    16#5051f4a7#, 16#537e4165#, 16#c31a17a4#, 16#963a275e#,
    16#cb3bab6b#, 16#f11f9d45#, 16#abacfa58#, 16#934be303#,
    16#552030fa#, 16#f6ad766d#, 16#9188cc76#, 16#25f5024c#,
    16#fc4fe5d7#, 16#d7c52acb#, 16#80263544#, 16#8fb562a3#,
    16#49deb15a#, 16#6725ba1b#, 16#9845ea0e#, 16#e15dfec0#,
    16#02c32f75#, 16#12814cf0#, 16#a38d4697#, 16#c66bd3f9#,
    16#e7038f5f#, 16#9515929c#, 16#ebbf6d7a#, 16#da955259#,
    16#2dd4be83#, 16#d3587421#, 16#2949e069#, 16#448ec9c8#,
    16#6a75c289#, 16#78f48e79#, 16#6b99583e#, 16#dd27b971#,
    16#b6bee14f#, 16#17f088ad#, 16#66c920ac#, 16#b47dce3a#,
    16#1863df4a#, 16#82e51a31#, 16#60975133#, 16#4562537f#,
    16#e0b16477#, 16#84bb6bae#, 16#1cfe81a0#, 16#94f9082b#,
    16#58704868#, 16#198f45fd#, 16#8794de6c#, 16#b7527bf8#,
    16#23ab73d3#, 16#e2724b02#, 16#57e31f8f#, 16#2a6655ab#,
    16#07b2eb28#, 16#032fb5c2#, 16#9a86c57b#, 16#a5d33708#,
    16#f2302887#, 16#b223bfa5#, 16#ba02036a#, 16#5ced1682#,
    16#2b8acf1c#, 16#92a779b4#, 16#f0f307f2#, 16#a14e69e2#,
    16#cd65daf4#, 16#d50605be#, 16#1fd13462#, 16#8ac4a6fe#,
    16#9d342e53#, 16#a0a2f355#, 16#32058ae1#, 16#75a4f6eb#,
    16#390b83ec#, 16#aa4060ef#, 16#065e719f#, 16#51bd6e10#,
    16#f93e218a#, 16#3d96dd06#, 16#aedd3e05#, 16#464de6bd#,
    16#b591548d#, 16#0571c45d#, 16#6f0406d4#, 16#ff605015#,
    16#241998fb#, 16#97d6bde9#, 16#cc894043#, 16#7767d99e#,
    16#bdb0e842#, 16#8807898b#, 16#38e7195b#, 16#db79c8ee#,
    16#47a17c0a#, 16#e97c420f#, 16#c9f8841e#, 16#00000000#,
    16#83098086#, 16#48322bed#, 16#ac1e1170#, 16#4e6c5a72#,
    16#fbfd0eff#, 16#560f8538#, 16#1e3daed5#, 16#27362d39#,
    16#640a0fd9#, 16#21685ca6#, 16#d19b5b54#, 16#3a24362e#,
    16#b10c0a67#, 16#0f9357e7#, 16#d2b4ee96#, 16#9e1b9b91#,
    16#4f80c0c5#, 16#a261dc20#, 16#695a774b#, 16#161c121a#,
    16#0ae293ba#, 16#e5c0a02a#, 16#433c22e0#, 16#1d121b17#,
    16#0b0e090d#, 16#adf28bc7#, 16#b92db6a8#, 16#c8141ea9#,
    16#8557f119#, 16#4caf7507#, 16#bbee99dd#, 16#fda37f60#,
    16#9ff70126#, 16#bc5c72f5#, 16#c544663b#, 16#345bfb7e#,
    16#768b4329#, 16#dccb23c6#, 16#68b6edfc#, 16#63b8e4f1#,
    16#cad731dc#, 16#10426385#, 16#40139722#, 16#2084c611#,
    16#7d854a24#, 16#f8d2bb3d#, 16#11aef932#, 16#6dc729a1#,
    16#4b1d9e2f#, 16#f3dcb230#, 16#ec0d8652#, 16#d077c1e3#,
    16#6c2bb316#, 16#99a970b9#, 16#fa119448#, 16#2247e964#,
    16#c4a8fc8c#, 16#1aa0f03f#, 16#d8567d2c#, 16#ef223390#,
    16#c787494e#, 16#c1d938d1#, 16#fe8ccaa2#, 16#3698d40b#,
    16#cfa6f581#, 16#28a57ade#, 16#26dab78e#, 16#a43fadbf#,
    16#e42c3a9d#, 16#0d507892#, 16#9b6a5fcc#, 16#62547e46#,
    16#c2f68d13#, 16#e890d8b8#, 16#5e2e39f7#, 16#f582c3af#,
    16#be9f5d80#, 16#7c69d093#, 16#a96fd52d#, 16#b3cf2512#,
    16#3bc8ac99#, 16#a710187d#, 16#6ee89c63#, 16#7bdb3bbb#,
    16#09cd2678#, 16#f46e5918#, 16#01ec9ab7#, 16#a8834f9a#,
    16#65e6956e#, 16#7eaaffe6#, 16#0821bccf#, 16#e6ef15e8#,
    16#d9bae79b#, 16#ce4a6f36#, 16#d4ea9f09#, 16#d629b07c#,
    16#af31a4b2#, 16#312a3f23#, 16#30c6a594#, 16#c035a266#,
    16#37744ebc#, 16#a6fc82ca#, 16#b0e090d0#, 16#1533a7d8#,
    16#4af10498#, 16#f741ecda#, 16#0e7fcd50#, 16#2f1791f6#,
    16#8d764dd6#, 16#4d43efb0#, 16#54ccaa4d#, 16#dfe49604#,
    16#e39ed1b5#, 16#1b4c6a88#, 16#b8c12c1f#, 16#7f466551#,
    16#049d5eea#, 16#5d018c35#, 16#73fa8774#, 16#2efb0b41#,
    16#5ab3671d#, 16#5292dbd2#, 16#33e91056#, 16#136dd647#,
    16#8c9ad761#, 16#7a37a10c#, 16#8e59f814#, 16#89eb133c#,
    16#eecea927#, 16#35b761c9#, 16#ede11ce5#, 16#3c7a47b1#,
    16#599cd2df#, 16#3f55f273#, 16#791814ce#, 16#bf73c737#,
    16#ea53f7cd#, 16#5b5ffdaa#, 16#14df3d6f#, 16#867844db#,
    16#81caaff3#, 16#3eb968c4#, 16#2c382434#, 16#5fc2a340#,
    16#72161dc3#, 16#0cbce225#, 16#8b283c49#, 16#41ff0d95#,
    16#7139a801#, 16#de080cb3#, 16#9cd8b4e4#, 16#906456c1#,
    16#617bcb84#, 16#70d532b6#, 16#74486c5c#, 16#42d0b857#
  );
  
  Td2: constant word_table := word_table'(
    16#a75051f4#, 16#65537e41#, 16#a4c31a17#, 16#5e963a27#,
    16#6bcb3bab#, 16#45f11f9d#, 16#58abacfa#, 16#03934be3#,
    16#fa552030#, 16#6df6ad76#, 16#769188cc#, 16#4c25f502#,
    16#d7fc4fe5#, 16#cbd7c52a#, 16#44802635#, 16#a38fb562#,
    16#5a49deb1#, 16#1b6725ba#, 16#0e9845ea#, 16#c0e15dfe#,
    16#7502c32f#, 16#f012814c#, 16#97a38d46#, 16#f9c66bd3#,
    16#5fe7038f#, 16#9c951592#, 16#7aebbf6d#, 16#59da9552#,
    16#832dd4be#, 16#21d35874#, 16#692949e0#, 16#c8448ec9#,
    16#896a75c2#, 16#7978f48e#, 16#3e6b9958#, 16#71dd27b9#,
    16#4fb6bee1#, 16#ad17f088#, 16#ac66c920#, 16#3ab47dce#,
    16#4a1863df#, 16#3182e51a#, 16#33609751#, 16#7f456253#,
    16#77e0b164#, 16#ae84bb6b#, 16#a01cfe81#, 16#2b94f908#,
    16#68587048#, 16#fd198f45#, 16#6c8794de#, 16#f8b7527b#,
    16#d323ab73#, 16#02e2724b#, 16#8f57e31f#, 16#ab2a6655#,
    16#2807b2eb#, 16#c2032fb5#, 16#7b9a86c5#, 16#08a5d337#,
    16#87f23028#, 16#a5b223bf#, 16#6aba0203#, 16#825ced16#,
    16#1c2b8acf#, 16#b492a779#, 16#f2f0f307#, 16#e2a14e69#,
    16#f4cd65da#, 16#bed50605#, 16#621fd134#, 16#fe8ac4a6#,
    16#539d342e#, 16#55a0a2f3#, 16#e132058a#, 16#eb75a4f6#,
    16#ec390b83#, 16#efaa4060#, 16#9f065e71#, 16#1051bd6e#,
    16#8af93e21#, 16#063d96dd#, 16#05aedd3e#, 16#bd464de6#,
    16#8db59154#, 16#5d0571c4#, 16#d46f0406#, 16#15ff6050#,
    16#fb241998#, 16#e997d6bd#, 16#43cc8940#, 16#9e7767d9#,
    16#42bdb0e8#, 16#8b880789#, 16#5b38e719#, 16#eedb79c8#,
    16#0a47a17c#, 16#0fe97c42#, 16#1ec9f884#, 16#00000000#,
    16#86830980#, 16#ed48322b#, 16#70ac1e11#, 16#724e6c5a#,
    16#fffbfd0e#, 16#38560f85#, 16#d51e3dae#, 16#3927362d#,
    16#d9640a0f#, 16#a621685c#, 16#54d19b5b#, 16#2e3a2436#,
    16#67b10c0a#, 16#e70f9357#, 16#96d2b4ee#, 16#919e1b9b#,
    16#c54f80c0#, 16#20a261dc#, 16#4b695a77#, 16#1a161c12#,
    16#ba0ae293#, 16#2ae5c0a0#, 16#e0433c22#, 16#171d121b#,
    16#0d0b0e09#, 16#c7adf28b#, 16#a8b92db6#, 16#a9c8141e#,
    16#198557f1#, 16#074caf75#, 16#ddbbee99#, 16#60fda37f#,
    16#269ff701#, 16#f5bc5c72#, 16#3bc54466#, 16#7e345bfb#,
    16#29768b43#, 16#c6dccb23#, 16#fc68b6ed#, 16#f163b8e4#,
    16#dccad731#, 16#85104263#, 16#22401397#, 16#112084c6#,
    16#247d854a#, 16#3df8d2bb#, 16#3211aef9#, 16#a16dc729#,
    16#2f4b1d9e#, 16#30f3dcb2#, 16#52ec0d86#, 16#e3d077c1#,
    16#166c2bb3#, 16#b999a970#, 16#48fa1194#, 16#642247e9#,
    16#8cc4a8fc#, 16#3f1aa0f0#, 16#2cd8567d#, 16#90ef2233#,
    16#4ec78749#, 16#d1c1d938#, 16#a2fe8cca#, 16#0b3698d4#,
    16#81cfa6f5#, 16#de28a57a#, 16#8e26dab7#, 16#bfa43fad#,
    16#9de42c3a#, 16#920d5078#, 16#cc9b6a5f#, 16#4662547e#,
    16#13c2f68d#, 16#b8e890d8#, 16#f75e2e39#, 16#aff582c3#,
    16#80be9f5d#, 16#937c69d0#, 16#2da96fd5#, 16#12b3cf25#,
    16#993bc8ac#, 16#7da71018#, 16#636ee89c#, 16#bb7bdb3b#,
    16#7809cd26#, 16#18f46e59#, 16#b701ec9a#, 16#9aa8834f#,
    16#6e65e695#, 16#e67eaaff#, 16#cf0821bc#, 16#e8e6ef15#,
    16#9bd9bae7#, 16#36ce4a6f#, 16#09d4ea9f#, 16#7cd629b0#,
    16#b2af31a4#, 16#23312a3f#, 16#9430c6a5#, 16#66c035a2#,
    16#bc37744e#, 16#caa6fc82#, 16#d0b0e090#, 16#d81533a7#,
    16#984af104#, 16#daf741ec#, 16#500e7fcd#, 16#f62f1791#,
    16#d68d764d#, 16#b04d43ef#, 16#4d54ccaa#, 16#04dfe496#,
    16#b5e39ed1#, 16#881b4c6a#, 16#1fb8c12c#, 16#517f4665#,
    16#ea049d5e#, 16#355d018c#, 16#7473fa87#, 16#412efb0b#,
    16#1d5ab367#, 16#d25292db#, 16#5633e910#, 16#47136dd6#,
    16#618c9ad7#, 16#0c7a37a1#, 16#148e59f8#, 16#3c89eb13#,
    16#27eecea9#, 16#c935b761#, 16#e5ede11c#, 16#b13c7a47#,
    16#df599cd2#, 16#733f55f2#, 16#ce791814#, 16#37bf73c7#,
    16#cdea53f7#, 16#aa5b5ffd#, 16#6f14df3d#, 16#db867844#,
    16#f381caaf#, 16#c43eb968#, 16#342c3824#, 16#405fc2a3#,
    16#c372161d#, 16#250cbce2#, 16#498b283c#, 16#9541ff0d#,
    16#017139a8#, 16#b3de080c#, 16#e49cd8b4#, 16#c1906456#,
    16#84617bcb#, 16#b670d532#, 16#5c74486c#, 16#5742d0b8#
  );
  
  Td3: constant word_table := word_table'(
    16#f4a75051#, 16#4165537e#, 16#17a4c31a#, 16#275e963a#,
    16#ab6bcb3b#, 16#9d45f11f#, 16#fa58abac#, 16#e303934b#,
    16#30fa5520#, 16#766df6ad#, 16#cc769188#, 16#024c25f5#,
    16#e5d7fc4f#, 16#2acbd7c5#, 16#35448026#, 16#62a38fb5#,
    16#b15a49de#, 16#ba1b6725#, 16#ea0e9845#, 16#fec0e15d#,
    16#2f7502c3#, 16#4cf01281#, 16#4697a38d#, 16#d3f9c66b#,
    16#8f5fe703#, 16#929c9515#, 16#6d7aebbf#, 16#5259da95#,
    16#be832dd4#, 16#7421d358#, 16#e0692949#, 16#c9c8448e#,
    16#c2896a75#, 16#8e7978f4#, 16#583e6b99#, 16#b971dd27#,
    16#e14fb6be#, 16#88ad17f0#, 16#20ac66c9#, 16#ce3ab47d#,
    16#df4a1863#, 16#1a3182e5#, 16#51336097#, 16#537f4562#,
    16#6477e0b1#, 16#6bae84bb#, 16#81a01cfe#, 16#082b94f9#,
    16#48685870#, 16#45fd198f#, 16#de6c8794#, 16#7bf8b752#,
    16#73d323ab#, 16#4b02e272#, 16#1f8f57e3#, 16#55ab2a66#,
    16#eb2807b2#, 16#b5c2032f#, 16#c57b9a86#, 16#3708a5d3#,
    16#2887f230#, 16#bfa5b223#, 16#036aba02#, 16#16825ced#,
    16#cf1c2b8a#, 16#79b492a7#, 16#07f2f0f3#, 16#69e2a14e#,
    16#daf4cd65#, 16#05bed506#, 16#34621fd1#, 16#a6fe8ac4#,
    16#2e539d34#, 16#f355a0a2#, 16#8ae13205#, 16#f6eb75a4#,
    16#83ec390b#, 16#60efaa40#, 16#719f065e#, 16#6e1051bd#,
    16#218af93e#, 16#dd063d96#, 16#3e05aedd#, 16#e6bd464d#,
    16#548db591#, 16#c45d0571#, 16#06d46f04#, 16#5015ff60#,
    16#98fb2419#, 16#bde997d6#, 16#4043cc89#, 16#d99e7767#,
    16#e842bdb0#, 16#898b8807#, 16#195b38e7#, 16#c8eedb79#,
    16#7c0a47a1#, 16#420fe97c#, 16#841ec9f8#, 16#00000000#,
    16#80868309#, 16#2bed4832#, 16#1170ac1e#, 16#5a724e6c#,
    16#0efffbfd#, 16#8538560f#, 16#aed51e3d#, 16#2d392736#,
    16#0fd9640a#, 16#5ca62168#, 16#5b54d19b#, 16#362e3a24#,
    16#0a67b10c#, 16#57e70f93#, 16#ee96d2b4#, 16#9b919e1b#,
    16#c0c54f80#, 16#dc20a261#, 16#774b695a#, 16#121a161c#,
    16#93ba0ae2#, 16#a02ae5c0#, 16#22e0433c#, 16#1b171d12#,
    16#090d0b0e#, 16#8bc7adf2#, 16#b6a8b92d#, 16#1ea9c814#,
    16#f1198557#, 16#75074caf#, 16#99ddbbee#, 16#7f60fda3#,
    16#01269ff7#, 16#72f5bc5c#, 16#663bc544#, 16#fb7e345b#,
    16#4329768b#, 16#23c6dccb#, 16#edfc68b6#, 16#e4f163b8#,
    16#31dccad7#, 16#63851042#, 16#97224013#, 16#c6112084#,
    16#4a247d85#, 16#bb3df8d2#, 16#f93211ae#, 16#29a16dc7#,
    16#9e2f4b1d#, 16#b230f3dc#, 16#8652ec0d#, 16#c1e3d077#,
    16#b3166c2b#, 16#70b999a9#, 16#9448fa11#, 16#e9642247#,
    16#fc8cc4a8#, 16#f03f1aa0#, 16#7d2cd856#, 16#3390ef22#,
    16#494ec787#, 16#38d1c1d9#, 16#caa2fe8c#, 16#d40b3698#,
    16#f581cfa6#, 16#7ade28a5#, 16#b78e26da#, 16#adbfa43f#,
    16#3a9de42c#, 16#78920d50#, 16#5fcc9b6a#, 16#7e466254#,
    16#8d13c2f6#, 16#d8b8e890#, 16#39f75e2e#, 16#c3aff582#,
    16#5d80be9f#, 16#d0937c69#, 16#d52da96f#, 16#2512b3cf#,
    16#ac993bc8#, 16#187da710#, 16#9c636ee8#, 16#3bbb7bdb#,
    16#267809cd#, 16#5918f46e#, 16#9ab701ec#, 16#4f9aa883#,
    16#956e65e6#, 16#ffe67eaa#, 16#bccf0821#, 16#15e8e6ef#,
    16#e79bd9ba#, 16#6f36ce4a#, 16#9f09d4ea#, 16#b07cd629#,
    16#a4b2af31#, 16#3f23312a#, 16#a59430c6#, 16#a266c035#,
    16#4ebc3774#, 16#82caa6fc#, 16#90d0b0e0#, 16#a7d81533#,
    16#04984af1#, 16#ecdaf741#, 16#cd500e7f#, 16#91f62f17#,
    16#4dd68d76#, 16#efb04d43#, 16#aa4d54cc#, 16#9604dfe4#,
    16#d1b5e39e#, 16#6a881b4c#, 16#2c1fb8c1#, 16#65517f46#,
    16#5eea049d#, 16#8c355d01#, 16#877473fa#, 16#0b412efb#,
    16#671d5ab3#, 16#dbd25292#, 16#105633e9#, 16#d647136d#,
    16#d7618c9a#, 16#a10c7a37#, 16#f8148e59#, 16#133c89eb#,
    16#a927eece#, 16#61c935b7#, 16#1ce5ede1#, 16#47b13c7a#,
    16#d2df599c#, 16#f2733f55#, 16#14ce7918#, 16#c737bf73#,
    16#f7cdea53#, 16#fdaa5b5f#, 16#3d6f14df#, 16#44db8678#,
    16#aff381ca#, 16#68c43eb9#, 16#24342c38#, 16#a3405fc2#,
    16#1dc37216#, 16#e2250cbc#, 16#3c498b28#, 16#0d9541ff#,
    16#a8017139#, 16#0cb3de08#, 16#b4e49cd8#, 16#56c19064#,
    16#cb84617b#, 16#32b670d5#, 16#6c5c7448#, 16#b85742d0#
  );
  
  Td4: constant word_table := word_table'(
    16#52525252#, 16#09090909#, 16#6a6a6a6a#, 16#d5d5d5d5#,
    16#30303030#, 16#36363636#, 16#a5a5a5a5#, 16#38383838#,
    16#bfbfbfbf#, 16#40404040#, 16#a3a3a3a3#, 16#9e9e9e9e#,
    16#81818181#, 16#f3f3f3f3#, 16#d7d7d7d7#, 16#fbfbfbfb#,
    16#7c7c7c7c#, 16#e3e3e3e3#, 16#39393939#, 16#82828282#,
    16#9b9b9b9b#, 16#2f2f2f2f#, 16#ffffffff#, 16#87878787#,
    16#34343434#, 16#8e8e8e8e#, 16#43434343#, 16#44444444#,
    16#c4c4c4c4#, 16#dededede#, 16#e9e9e9e9#, 16#cbcbcbcb#,
    16#54545454#, 16#7b7b7b7b#, 16#94949494#, 16#32323232#,
    16#a6a6a6a6#, 16#c2c2c2c2#, 16#23232323#, 16#3d3d3d3d#,
    16#eeeeeeee#, 16#4c4c4c4c#, 16#95959595#, 16#0b0b0b0b#,
    16#42424242#, 16#fafafafa#, 16#c3c3c3c3#, 16#4e4e4e4e#,
    16#08080808#, 16#2e2e2e2e#, 16#a1a1a1a1#, 16#66666666#,
    16#28282828#, 16#d9d9d9d9#, 16#24242424#, 16#b2b2b2b2#,
    16#76767676#, 16#5b5b5b5b#, 16#a2a2a2a2#, 16#49494949#,
    16#6d6d6d6d#, 16#8b8b8b8b#, 16#d1d1d1d1#, 16#25252525#,
    16#72727272#, 16#f8f8f8f8#, 16#f6f6f6f6#, 16#64646464#,
    16#86868686#, 16#68686868#, 16#98989898#, 16#16161616#,
    16#d4d4d4d4#, 16#a4a4a4a4#, 16#5c5c5c5c#, 16#cccccccc#,
    16#5d5d5d5d#, 16#65656565#, 16#b6b6b6b6#, 16#92929292#,
    16#6c6c6c6c#, 16#70707070#, 16#48484848#, 16#50505050#,
    16#fdfdfdfd#, 16#edededed#, 16#b9b9b9b9#, 16#dadadada#,
    16#5e5e5e5e#, 16#15151515#, 16#46464646#, 16#57575757#,
    16#a7a7a7a7#, 16#8d8d8d8d#, 16#9d9d9d9d#, 16#84848484#,
    16#90909090#, 16#d8d8d8d8#, 16#abababab#, 16#00000000#,
    16#8c8c8c8c#, 16#bcbcbcbc#, 16#d3d3d3d3#, 16#0a0a0a0a#,
    16#f7f7f7f7#, 16#e4e4e4e4#, 16#58585858#, 16#05050505#,
    16#b8b8b8b8#, 16#b3b3b3b3#, 16#45454545#, 16#06060606#,
    16#d0d0d0d0#, 16#2c2c2c2c#, 16#1e1e1e1e#, 16#8f8f8f8f#,
    16#cacacaca#, 16#3f3f3f3f#, 16#0f0f0f0f#, 16#02020202#,
    16#c1c1c1c1#, 16#afafafaf#, 16#bdbdbdbd#, 16#03030303#,
    16#01010101#, 16#13131313#, 16#8a8a8a8a#, 16#6b6b6b6b#,
    16#3a3a3a3a#, 16#91919191#, 16#11111111#, 16#41414141#,
    16#4f4f4f4f#, 16#67676767#, 16#dcdcdcdc#, 16#eaeaeaea#,
    16#97979797#, 16#f2f2f2f2#, 16#cfcfcfcf#, 16#cececece#,
    16#f0f0f0f0#, 16#b4b4b4b4#, 16#e6e6e6e6#, 16#73737373#,
    16#96969696#, 16#acacacac#, 16#74747474#, 16#22222222#,
    16#e7e7e7e7#, 16#adadadad#, 16#35353535#, 16#85858585#,
    16#e2e2e2e2#, 16#f9f9f9f9#, 16#37373737#, 16#e8e8e8e8#,
    16#1c1c1c1c#, 16#75757575#, 16#dfdfdfdf#, 16#6e6e6e6e#,
    16#47474747#, 16#f1f1f1f1#, 16#1a1a1a1a#, 16#71717171#,
    16#1d1d1d1d#, 16#29292929#, 16#c5c5c5c5#, 16#89898989#,
    16#6f6f6f6f#, 16#b7b7b7b7#, 16#62626262#, 16#0e0e0e0e#,
    16#aaaaaaaa#, 16#18181818#, 16#bebebebe#, 16#1b1b1b1b#,
    16#fcfcfcfc#, 16#56565656#, 16#3e3e3e3e#, 16#4b4b4b4b#,
    16#c6c6c6c6#, 16#d2d2d2d2#, 16#79797979#, 16#20202020#,
    16#9a9a9a9a#, 16#dbdbdbdb#, 16#c0c0c0c0#, 16#fefefefe#,
    16#78787878#, 16#cdcdcdcd#, 16#5a5a5a5a#, 16#f4f4f4f4#,
    16#1f1f1f1f#, 16#dddddddd#, 16#a8a8a8a8#, 16#33333333#,
    16#88888888#, 16#07070707#, 16#c7c7c7c7#, 16#31313131#,
    16#b1b1b1b1#, 16#12121212#, 16#10101010#, 16#59595959#,
    16#27272727#, 16#80808080#, 16#ecececec#, 16#5f5f5f5f#,
    16#60606060#, 16#51515151#, 16#7f7f7f7f#, 16#a9a9a9a9#,
    16#19191919#, 16#b5b5b5b5#, 16#4a4a4a4a#, 16#0d0d0d0d#,
    16#2d2d2d2d#, 16#e5e5e5e5#, 16#7a7a7a7a#, 16#9f9f9f9f#,
    16#93939393#, 16#c9c9c9c9#, 16#9c9c9c9c#, 16#efefefef#,
    16#a0a0a0a0#, 16#e0e0e0e0#, 16#3b3b3b3b#, 16#4d4d4d4d#,
    16#aeaeaeae#, 16#2a2a2a2a#, 16#f5f5f5f5#, 16#b0b0b0b0#,
    16#c8c8c8c8#, 16#ebebebeb#, 16#bbbbbbbb#, 16#3c3c3c3c#,
    16#83838383#, 16#53535353#, 16#99999999#, 16#61616161#,
    16#17171717#, 16#2b2b2b2b#, 16#04040404#, 16#7e7e7e7e#,
    16#babababa#, 16#77777777#, 16#d6d6d6d6#, 16#26262626#,
    16#e1e1e1e1#, 16#69696969#, 16#14141414#, 16#63636363#,
    16#55555555#, 16#21212121#, 16#0c0c0c0c#, 16#7d7d7d7d#
  );

  rcon: constant rcon_array := rcon_array'(
    16#01000000#, 16#02000000#, 16#04000000#, 16#08000000#,
    16#10000000#, 16#20000000#, 16#40000000#, 16#80000000#,
    16#1B000000#, 16#36000000#
  );

  subtype byte_index is Integer range 0 .. 15;
  type block is array (byte_index) of byte;

  subtype key_index is Integer range 0 .. 4*MAXKC-1;
  type key is array(key_index) of byte;
  subtype roundkey_index is Integer range 0 .. 4*(MAXNR+1)-1;
  type key_schedule is array(roundkey_index) of word;

  function Shift_Left(value: word; amount: Natural) return word;
  function Shift_Right(value: word; amount: Natural) return word;

  function CombineWord(b0, b1, b2, b3: byte) return word;
  procedure SplitWord(w: in word; b0, b1, b2, b3: out byte);
  --# derives b0, b1, b2, b3 from w;

  procedure KeySetupEnc(rk: out key_schedule; cipherKey: in key; Nk: in Integer; Nr: out Integer);
  --# derives rk from cipherKey, Nk &
  --#         Nr from Nk;
  --# pre Nk = 4 OR Nk = 6 OR Nk = 8;

  procedure KeySetupDec(rk: out key_schedule; cipherKey: in key; Nk: in Integer; Nr: out Integer);
  --# derives rk from cipherKey, Nk &
  --#         Nr from Nk;
  --# pre Nk = 4 OR Nk = 6 OR Nk = 8;

  procedure aesKeySetupEnc(rk: out key_schedule; cipherKey: in key; keyBits: in Integer; Nr: out Integer);
  --# derives rk from cipherKey, keyBits &
  --#         Nr from keyBits;
  --# pre keyBits = 128 OR keyBits = 192 OR keyBits = 256;

  procedure aesKeySetupDec(rk: out key_schedule; cipherKey: in key; keyBits: in Integer; Nr: out Integer);
  --# derives rk from cipherKey, keyBits &
  --#         Nr from keyBits;
  --# pre keyBits = 128 OR keyBits = 192 OR keyBits = 256;

  procedure aesEncrypt(rk: in key_schedule; Nr: in Integer; pt: in block; ct: out block);
  --# derives ct from pt, rk, Nr;

  procedure aesDecrypt(rk: in key_schedule; Nr: in Integer; ct: in block; pt: out block);
  --# derives pt from ct, rk, Nr;
end AES;
